#include "structure.h"
#include "primitives_structure.h"

#include <stdlib.h>
#include <stdio.h>
#include <math.h>


/**** LITTERAL ****/
/* Cree un litteral */
Litteral* creerLitteral( int variable ){

	Litteral *l;

	l = ( Litteral* ) calloc(1, sizeof( Litteral ) );

	l->variable = variable;
	l->suivant = NULL;

	return l;
}

/* Ajoute un litteral l a une clause c */
void afficherLitteral( Litteral l ){

	printf("%cx%i", (l.variable>=0)?' ':'!', abs(l.variable));

}

/**** CLAUSE ****/
/* Cree une clause */
Clause* creerClause( ){

	Clause *c;

	c = ( Clause* ) malloc( sizeof( Clause ) );

	c->etat = INCONNU;
	c->card = 0;
	c->taille = 0;
	c->tete = NULL;

	return c;
}

/* Ajoute un litteral l a une clause c */
void afficherClause( Clause c, Formule f ){

	Litteral *l;

	printf("( %i, { ", c.card);
	FOREACH(l,c.tete){
		
		if( f.litteraux[abs(l->variable)].etat == INCONNU ){
			afficherLitteral(*l);
			printf(", ");
		}
	}
	printf(" } ) (%i)\n", c.taille);

}

/* Affiche une clause (debug) */
void ajouterLitteralClause( Clause *c, Litteral *l ){

	if(c->tete!=NULL)
		l->suivant = c->tete;
	c->tete = l;

}

/* Libere une clause de la memoire */
void freeClause( Clause *c ){

	Litteral *I, *prec=NULL;

	if( c==NULL ) return;

	FOREACH( I, c->tete ){

		if(prec!=NULL) free(prec);
		prec = I;

	}

	if( prec != NULL )
		free(prec);

	free(c);
	c = NULL;

}

/*** FORMULE ****/
/* Cree une formule */
Formule* creerFormule( ){

	Formule* f;

	f = ( Formule* ) malloc( sizeof( Formule ) );

	
	f->nbLitteraux = 0;
	f->nbClauses = 0;
	f->taille = 0;
	f->litteraux = NULL;
	f->clauses = NULL;
	

	return f;
}

/* Affiche une formule (debug) */
void afficherFormule( Formule f ){

	int i, premier = 1;
	printf("\n=== Formule ===\n");
	for( i=1; i<=f.nbClauses; i++ ){
		
		if( f.clauses[i]->etat == INCONNU )
		{
			if( premier == 1 ){
				
				printf(" ");
				premier = 0;
			}else printf("^");
			
			afficherClause( *(f.clauses[i]), f );
		}
	}

	printf("\nClauses restantes: %i\n", f.taille );
	printf("=== Fin Formule ===\n\n");
}

/* Libere une formule de la memoire */
void freeFormule( Formule *f ){

	int i;

	for( i=0; i<=f->taille; i++ )
		freeClause(f->clauses[i]);

	freeListeLitteraux( f->litteraux );

	free( f->clauses );

	free(f);
	f = NULL;

}

/* Charge une formule depuis l'entree standard */
Formule* chargerFormule( ){

	Formule *f;

	int i, j, v;
	char car;
	Clause *c;
	Litteral *l;
	ListeClause *listeClause;

	f = creerFormule( );

	// choix de la taille
	scanf("%i", &(f->taille));
	f->nbClauses = f->taille;
	getchar();

	// choix du nombre de litteraux
	scanf("%i", &(f->nbLitteraux) );
	getchar();

	// creation du tableau
	f->clauses = (Clause**) calloc( f->nbClauses+1, sizeof(Clause*) );
	
	// on cree la liste de litteraux
	f->litteraux = creerListeLitteraux( f->nbLitteraux );

	// creation des clauses
	for( i=1; i<=f->nbClauses; i++ ){

		c = creerClause();

		scanf(" ( %i , {", &(c->card) );

		car = '{';

		for( j=0; car!='}'; j++ ){

			scanf("%i", &v );

			//Ajoute le litteral a la clause
			l = creerLitteral( v );
			ajouterLitteralClause( c, l );
			
			//Ajoute la clause dans la liste de litteraux
			listeClause = creerListeClause( c, (v>0)?1:-1 );
			ajouterClauseListe( f->litteraux, abs(v), listeClause );

			scanf(" %c",&car);

		}

		// fin
		scanf(" )");
		getchar();

		c->taille = j;
		f->clauses[i] = c;

	}



	return f;

}

/**** LISTE DE CLAUSE ****/
/* Cree une liste de clause */
ListeClause* creerListeClause( Clause *c, int signe ){

	ListeClause *l;

	//Allocation
	l = ( ListeClause* ) malloc( sizeof( ListeClause ) );
	l->signe = signe;
	l->affectee = FAUX;
	l->clause = c;
	l->suivant = NULL;

	return l;
}

/* Libere la liste de clauses de la memoire */
void freeListeClause( ListeClause *l ){

	ListeClause *tmp;

	while(l!=NULL){

		tmp=l;
		l=l->suivant;
		free(tmp);

	}

}

/**** LISTE DE LITTERAUX ****/
/* Cree une liste de litteraux de taille nbLitteraux */
ListeLitteraux* creerListeLitteraux( int nbLitteraux ){

	ListeLitteraux *l;
	int i;
	//Allocation dynamique
	l = ( ListeLitteraux* ) calloc( nbLitteraux+1, sizeof( ListeLitteraux ) );
	
	
	for(i=0; i<=nbLitteraux; i++)
	{
		//Affectation de la taille
		l[i].taille = 0;
		//Etat inconnu
		l[i].etat = INCONNU;
		//initialisation de la liste
		l[i].litteraux = NULL;
	}

	return l;
}

/* Ajoute la clause a la liste de litteraux a l'emplacement i */
void ajouterClauseListe( ListeLitteraux *listeLitteraux, int i, ListeClause *c ){

	c->suivant = listeLitteraux[i].litteraux;
	listeLitteraux[i].litteraux = c;
	listeLitteraux[i].taille++;
}

/* Libere une liste de litteraux de la memoire */
void freeListeLitteraux( ListeLitteraux *l ){
	
	int i;
	ListeClause *tmp, *remove;
	
	for( i=0; i<=l->taille; i++){

		tmp = (l[i]).litteraux;

		while( tmp != NULL )
		{
			remove = tmp;
			tmp = tmp->suivant;
			freeListeClause(remove);
		}

	}
	
	free(l);
}

